combinatory 論理
combinatory logic。組み合はせ論理
SKI
複製$ Sxyz=xz(yz)。破毀$ Kxy=x。恆等$ Ix=x
$ I=SKK
$ \because SKKx=Kx(Kx)=x
$ I=SKS
$ SIIx=Ix(Ix)=xx自己適用
SKI
code:Unlambda
`skivdcer.@?|
BCKW
$ Bxyz=x(yz),$ Cxyz=xzy,$ Kxy=x,$ Wxy=xyy
SKI に依る飜譯
$ B=S(KS)K.
$ C=S(S(K(S(KS)K))S)(KK).
$ K=K.
$ W=SS(SK).
SKI を BCKW に飜譯する
$ I=WK.
$ K=K.
$ S=B(B(BW)C)(BB).
$ S=B(BW)(BBC).
$ B:$ (q \to r) \to ((p \to q) \to (p \to r))
$ C:$ (p \to (q \to r)) \to (q \to (p \to r))
$ K:$ p \to (q \to p)
$ W:$ (p \to (p \to q)) \to (p \to q)
BCKW から W を除いたものに對應する
BCK-λ計算
不動點 combinator (再歸)
Y combinator
$ Y=S(K(SII))(S(S(KS)K)(K(SII))),$ Yx=xYx
$ Y=(\lambda f.(\lambda x.f(x x))(\lambda x.f(x x))),$ Yg=g(Yg)
Z combinator
$ Z=\lambda f.(\lambda x.f(\lambda y.x x y))(\lambda x.f(\lambda y.x x y))
Turing's
$ \Theta =(\lambda x.\lambda y.(y(x x y)))(\lambda x.\lambda y.(y(x x y)))
$ \Theta_v =(\lambda x.\lambda y.(y(\lambda z.x x y z)))(\lambda x.\lambda y.(y(\lambda z.x x y z)))
shortest in SK
$ Y'=SSK(S(K(SS(S(SSK))))K)
$ Y'=(\lambda x.\lambda y.x y x)(\lambda y.\lambda x.y(x y x))
λ計算からの變換$ T\lbrack~\rbrack。abstraction elimination SKI
$ T\lbrack x\rbrack=x
$ T\lbrack(E_1~E_2)\rbrack=(T\lbrack E_1\rbrack~T\lbrack E_2\rbrack)
$ T\lbrack\lambda x.E\rbrack=(K~T\lbrack E\rbrack)if$ xdoes not occur free in$ E
$ T\lbrack\lambda x.x\rbrack=I
$ T\lbrack\lambda x.\lambda y.E\rbrack=T\lbrack\lambda x.T\lbrack\lambda y.E\rbrack\rbrackif$ xoccurs free in$ E
$ T\lbrack\lambda x.(E_1~E_2)\rbrack=(S~T\lbrack\lambda x.E_1\rbrack~T\lbrack\lambda x.E_2\rbrack)